package plp.imperative2.declaration;

import plp.expressions2.expression.Expressao;
import plp.expressions2.expression.Valor;
import plp.expressions2.memory.AmbienteExecucao;
import plp.expressions2.memory.IdentificadorJaDeclaradoException;
import plp.expressions2.memory.IdentificadorNaoDeclaradoException;
import plp.expressions2.memory.VariavelJaDeclaradaException;
import plp.expressions2.memory.VariavelNaoDeclaradaException;
import plp.imperative1.declaration.Declaracao;
import plp.imperative1.memory.AmbienteCompilacaoImperativa;
import plp.imperative1.memory.AmbienteExecucaoImperativa;
import plp.imperative1.memory.EntradaVaziaException;
import plp.imperative2.memory.ContextoExecucaoImperativa2;
import plp.imperative2.memory.ContratoException;

public class DeclaracaoInvariante extends Declaracao {

	private Expressao expressao;

	public DeclaracaoInvariante(Expressao expressao) {
		this.expressao = expressao;
	}

	Valor avaliar(AmbienteExecucao amb) throws VariavelNaoDeclaradaException,
			VariavelJaDeclaradaException {
		return expressao.avaliar(amb);
	}

	@Override
	public boolean checaTipo(AmbienteCompilacaoImperativa ambiente)
			throws IdentificadorJaDeclaradoException,
			IdentificadorNaoDeclaradoException, EntradaVaziaException {

		return expressao.checaTipo(ambiente)
				&& expressao.getTipo(ambiente).eBooleano();
	}

	@Override
	public AmbienteExecucaoImperativa elabora(
			AmbienteExecucaoImperativa ambiente)
			throws IdentificadorJaDeclaradoException,
			IdentificadorNaoDeclaradoException, EntradaVaziaException,
			ContratoException {

		((ContextoExecucaoImperativa2) ambiente).addInvariante(this);
		return ambiente;
	}
	
	@Override
	public String toString() {
		return expressao.toString();
	}
}
